/*
 * Term.h
 *
 *  Created on: May 3, 2011
 *      Author: trungtq
 */

#ifndef TERM_H_
#define TERM_H_

#include <vector>
#include <set>
#include <map>
#include <stdio.h>
#include <iostream>
#include "Function.h"
#include "Variable.h"
#include "CCException.h"
#include "CCOption.h"

enum TermType {TERMTYPE_VAR, TERMTYPE_FUNC, TERMTYPE_NULL};

using namespace std;


class Term {

public:
    Term();
    Term(TermType type);
    Term(Variable x);
    Term(Function f);
    Term(Function f, Term arg);
    Term(Function f, Term arg1, Term arg2);
    Term(Function f, Term arg1, Term arg2, Term arg3);
    Term(Function f, vector<Term> args);
    virtual ~Term();

private:
    enum TermType type;
    Variable variable;
    Function function;
    vector<Term> arguments;

public:
    // getter & setter
    Function getFunction() const;
    int getArgumentsSize() const;
    Term getArgument(int index) const;
    vector<Term> getArguments() const;
    Variable getVariable() const;

public:
    bool isInit();
    bool isVariable() const;
    bool isConstant() const;
    bool isFunction() const;
    bool isNULL() const;
    int getDepth();
    string toString() const;
    bool equal(Term other);

public:
    static Term parseString(string termString, FunctionSet* funcSet, VariableSet *varSet);
    static Term parseString(string termString);
    static Term parseString(const char* termString);
    static const Term NULLTerm;
};

class TermCompare {
public:
    bool operator() (Term term1, Term term2) {
        string s1 = term1.toString();
        string s2 = term2.toString();
        return (s1.compare(s2) < 0);
    }
};

typedef set<Term, TermCompare>        TermSet;
typedef map<Term, Term, TermCompare>  TermMap;
typedef vector<Term>                  TermList;
typedef pair<Term, Term>              TermPair;

class TermPairCompare {
public:
    bool operator() (TermPair pair1, TermPair pair2) {
        string s1 = pair1.first.toString() + pair1.second.toString();
        string s2 = pair2.first.toString() + pair2.second.toString();
        return (s1.compare(s2) < 0);
    }
};



#endif /* TERM_H_ */
